\documentclass[]{prezentare}
\graphicspath{{Imagini/}}

\title  {\texorpdfstring
            {Verificarea termin\u arii programelor cu ajutorul tipurilor}
            {Verificarea terminarii programelor cu ajutorul tipurilor}
        }

\author [Cristian T\u al\u au]
        {\texorpdfstring
            {{\bf Autor:} Cristian T\u al\u au \\ {\bf Conduc\u ator \c stiin\c tific:} Cristian Giumale}
            {Cristian Talau}
        }
\institute {\texorpdfstring
                {Universitatea "Politehnica" Bucure\c sti}
                {Universitatea "Politehnica" Bucuresti}
           }
\titlegraphic {}

% Marcouri
\newcommand\nat{\textbf{Nat}}
\newcommand\tlist{\textbf{List}}
\newcommand\sfrec{\text{$System\ F^{rec}\ $}}
\newcommand\sfhat{\text{$System\ F$\^{}}}
\newcommand\sysf{\text{$System\ F$}}

\newcommand\vdrec{\vdash_\text{$SysF^{rec}\ $}}
\newcommand\vdhat{\vdash_\text{$SysF$\^{}}}
\newcommand\vdtm{\vdash_\text{$SF$\^{}mon}}

\newcommand\kwd[1]{\textcolor[rgb]{0.54,0.21,0.22}{\textbf{#1}}}
\newcommand\typ[1]{\textcolor[rgb]{0.00,0.59,0.00}{\textit{#1}}}

\newcommand\av[3]{\visible<#1>{\alert<#2>{\text{\tiny #3}}}}

\begin{document}

    \begin{frame}
        \titlepage
    \end{frame}

%-----------------------------------------------------------------------------------
    \begin{frame}
        \frametitle{Problema verific\u arii statice}
        \begin{block}<+->{Instan\c t\u a - Terminarea programelor}
            \begin{itemize}
            \item Solu\c tie corect\u a dar incomplet\u a
            \item \^ In cadrul analizei de tip
            \item \sfrec = \sysf + \textbf{case} + \textbf{letrec}
            \end{itemize}
        \end{block}

        \begin{exampleblock}<+-> {Caracteristici}
            Tipuri \alert<2>{polimorfice}, \alert<3>{recursive}, \alert<4>{de ordin \^ inalt}
            $$\alert<3>{Tree}\ \alert<2>{X} = lf : \alert<3>{Tree}\ \alert<2>{X} \,|\, nd : \alert<4>{(Nat \to \alert<3>{Tree}\ \alert<2>{X})} \to \alert<2>{X} \to \alert<3>{Tree}\ \alert<2>{X}$$
        \end{exampleblock}

    \end{frame}
%-----------------------------------------------------------------------------------
    \begin{frame}
        \frametitle{Ideea \sfhat}

        \begin{block}<1->{Constr\^ angere letrec}
        \begin{itemize}
        \item Apelurile recursive se fac cu argumente mai mici
        \item Rela\c tia de ordine $\Leftrightarrow$ Rela\c tia de subtip
        \end{itemize}

        \end{block}
        \frametitle{Tipuri inductive cu dimensiune}
        \begin{exampleblock}<2->{\visible<3->{\sfhat} \visible<2>{\sfrec} }
                \vskip -0.6cm
                \begin{align*}
                    \textbf{Datatype}\ Nat &= z : Nat^{\visible<3->{\alert{\widehat{\imath}}}} \,|\,
                                              s : Nat^{\visible<3->{\alert{\imath}}} \to Nat^{\visible<3->{\alert{\widehat{\imath}}}} \\
                    \textbf{Datatype}\ List &= nil : List^{\visible<3->{\alert{\widehat{\imath}}}} \,|\, cons : Nat^{\visible<3->{\alert{\infty}}} \to List^{\visible<3->{\alert{\imath}}} \to List^{\visible<3->{\alert{\widehat{\imath}}}}
                \end{align*}
        \end{exampleblock}
        \begin{exampleblock}<2->{Diagrama}
        \begin{center}
            \begin{tikzpicture}
                \path[rounded corners,use as bounding box] (0,0) rectangle (10cm,-2.2cm);
                \tikzstyle{nat} = [shape=circle,draw=black, thin]
                \tikzstyle{natinv} = [shape=circle]
                \tikzstyle{constr} = [>=latex',draw, ->,color=blue!50!black , thick];

                % z - constructor , Diagrama System F
                \path<2->[constr]  (3.5cm,-1.1cm) node[left] {\scriptsize z}  to (5cm,-1.1cm);
                \node<2>[nat,minimum size=2.1cm,pin={[pin edge={<-,red}]-20:$\nat$}] at (5cm,-1.1cm) (natinfty) {};
                \path<2>[constr] (natinfty.-150) node[right] {\scriptsize s} parabola[bend pos=0.5] bend +(0,-0.4cm) (natinfty.-100);

                % nat^{d^}
                \node<3->[nat,minimum size=0.8cm,pin={[pin edge={<-,red}]40:$\nat^{\widehat{d}}$}] at (5cm,-1.1cm) (natd) {};
                \node[natinv,minimum size=1.1cm] at (5cm,-1.1cm) (nathd) {};
                \path<4->[constr] (natd.-160) node[right] {\scriptsize s} parabola[bend pos=0.6] bend +(0,-0.4cm) (nathd.-110) ;

                % nat^{d^^}
                \node<5->[nat,minimum size=1.1cm,pin={[pin edge={<-,red}]0:$\nat^{\widehat{\widehat{d}}}$}] at (5cm,-1.1cm) (nathd) {};

                % nat^\infty
                \node<6>[nat,minimum size=2.1cm,pin={[pin edge={<-,red}]-20:$\nat^{\infty}$}] at (5cm,-1.1cm) (natinfty) {};
                \node<6>[above of=natd,yshift=-0.12cm] (dots) {$\vdots$};
                \path<6>[constr] (natinfty.-150) node[right] {\scriptsize s} parabola[bend pos=0.5] bend +(0,-0.4cm) (natinfty.-100);
            \end{tikzpicture}
        \end{center}
        \end{exampleblock}

    \end{frame}
%-----------------------------------------------------------------------------------
    \begin{frame}
        \frametitle{Expresivitate}
        \begin{block}<1->{Propriet\u ati - \sfhat}
            \begin{itemize}
                \item Compatibilitate \sfrec
                \item Normalizare puternic\u a \visible<2->{\alert<2>{$\Longrightarrow$ Incompletitudine Turing}}
            \end{itemize}
        \end{block}
        \begin{block}<3->{Tipuri monadice - \sfhat-mon}
            \begin{itemize}
                \item Dou\u a categorii de tipuri incompatibile ca $\sqsubseteq$: \textbf{ID} , \textbf{NT}
                \item \textbf{ID} - toate expresiile \sfhat
                \item \textbf{NT} - expresii \sfrec (slab/ne)-normalizabile 
            \end{itemize}
        \end{block}


    \end{frame}
%-----------------------------------------------------------------------------------
    \begin{frame}
        \frametitle{Cum construim expresii NT?}

        \begin{exampleblock}
        {\visible<1-3>{unit}
         {\visible<4>{letrec - $Nat_{nt}^{\imath} \sqsubseteq Nat_{nt}^{\jmath}$}
          \visible<5->{bind}
         }
        }
        
        \tikz[remember picture,baseline=-.5ex] \node[] (n6) {};
        $\textbf{bind}\ \omega Nat$\\
        $ \qquad \lambda e. \textbf{bind}\ \omega Fz$ \\
        $ \qquad \qquad \lambda fz $
        \tikz[remember picture,baseline=-.5ex] \node[] (n5) {$.\textbf{bind}$};
        \tikz[remember picture,baseline=-.5ex] \node[] (n4) {$\omega Fs$}; \\
        $ \qquad \qquad \qquad$
        \tikz[remember picture,baseline=-.5ex] \node[] (n3) {$\lambda fs .$};
        \tikz[remember picture,baseline=-.5ex] \node[] (n2) {\textbf{unit}} ;
        \tikz[remember picture,baseline=-.5ex] \node[] (n1) {$(case\ e \ of\ \{z \Rightarrow fz | s \Rightarrow fs \})$};

        \begin{tikzpicture}[remember picture]
                \node<1>[draw,rounded corners, thick, color=red, overlay, fit=(n1)] (m1) {};                    % case-ul
                \node<2>[draw,rounded corners, thick, color=red, overlay, fit=(n1) (n2)] (m2) {};               % unit-ul
                \node<3>[draw,rounded corners, thick, color=red, overlay, fit=(n1) (n2) (n3)] (m3) {};          % lambda
                \node<4>[draw,rounded corners, thick, color=red, overlay, fit=(n4)] (m4) {};                    % oFn - nonterm
                \node<5-6>[draw,rounded corners, thick, color=red, overlay, fit=(n1) (n2) (n3) (n5)] (m5) {};   % bind
        \end{tikzpicture}

        \end{exampleblock}

        \begin{exampleblock}{Diagram\u a}
        \begin{center}
            \begin{tikzpicture}[auto,>=latex', remember picture]
                \tikzstyle{monad} = [draw=black, thick,shape=rectangle, rounded corners, minimum height=2.4cm,minimum width=1.5cm];
                \tikzstyle{operator} = [>=latex', draw, ->, color=brown!60!black, thick, dashed];
                \tikzstyle{expresie} = [overlay, >=latex', draw, ->, color=red!60!black, thick]
                \path[rounded corners,use as bounding box] (0,0) rectangle (10.0cm,-2.6cm);

                % ID & NT
                \node[monad] at (3.3cm,-1.3cm) (id) {ID};
                \node[monad] at (6.7cm,-1.3cm) (nt) {NT};

                % case -ul
                \node<1-2>[shape=circle, draw=red,minimum size=0.3] at (3.3cm, -1.7 cm) (caseID) {};
                \path<1>[expresie] (m1) to[bend right] (caseID);

                % unit-ul
                \node<2>[shape=circle, draw=red,minimum size=0.3] at (6.7cm, -1.7 cm) (caseNT) {};
                \path<2>[operator] (caseID) to[bend right] node[above] {\scriptsize \textbf{unit}} (caseNT);
                \path<2>[expresie] (m2) to[bend left] (caseNT);

                % functia
                \path<3-6>[draw,->,color=red,very thick] (id.-40) to node[above] (nod) {} (nt.-140);
                \path<3>[expresie] (m3) to (nod);

                % oFns
                \node<4-6>[shape=circle, draw=red,minimum size=0.3,pin={[pin edge={<-,red}]45:{\scriptsize $letrec_{Nat \to Nat} f = f$}}]
                    at (6.7cm, -0.9 cm) (oFns) {};
                \path<4>[expresie] (m4) to[bend left] (oFns);

                % bind-ul pe pasi
                \node<5-6>[shape=circle, draw=brown!60!black, dashed, minimum size=0.3] at (3.3cm, -0.9 cm) (oFnsID) {};
                \path<5-6>[operator] (oFns.west) to[bend right] node[above] {\scriptsize \textbf{bind}} (oFnsID.east);
                \path<6>[operator] (oFnsID.south) to[bend right] (id.-40);
                \path<6>[operator] (id.-40) to[bend right] (nt.-140);

                % rezultatul final
                \node<6>[shape=circle, draw=red, minimum size=0.3] at (6.7cm, -1.7 cm) (bindNT) {};
                \path<6>[operator] (nt.-140) to[bend right] (bindNT.west);
            \end{tikzpicture}
        \end{center}
        \end{exampleblock}
    \end{frame}
%-----------------------------------------------------------------------------------
    \begin{frame}
        \frametitle{Tipuri monadice - propriet\u a\c ti}
        \begin{block}{Propriet\u ati}
        \begin{itemize}
        \item {\bf Siguran\c t\u a}:
            \begin{itemize}
                \item \textit{(Conservare)} Dac\u a $e:\tau \to e':\tau'$, atunci.
                    \begin{itemize}
                        \item $\tau \in \textbf{ID} \Rightarrow \tau = \tau'$
                        \item $\tau \in \textbf{NT} \Rightarrow |\tau| = |\tau'|$.
                    \end{itemize}
                \item \textit{(Progres)} Evaluarea unei expresii se termin\u a cu o valoare.
            \end{itemize}
        \item {\bf Normalizare puternic\u a}
            \begin{itemize}
                \item Pentru tipuri din \textbf{ID}.
            \end{itemize}
        \item {\bf Completitudine Turing}
            \begin{itemize}
                \item Orice func\c tie $\mu$-recursiv\u a poate fi tipat\u a \^ in \textbf{NT}
            \end{itemize}
        \item {\bf Compatibilitate} cu \sfrec
        \end{itemize}
        \end{block}
    \end{frame}
%-----------------------------------------------------------------------------------

    \begin{frame}
        \frametitle{TBT (Type Based Termination) }
        \begin{block}<+->{Sintax\u a $\approx$ ML}
                \vskip -0.6cm
            \begin{align*}
                \texttt{\kwd{Inductive} \typ{Bool} }& \texttt{= t : \typ{Bool} | f : \typ{Bool}} \\
                \lambda x : Nat . e                 &\mapsto                \texttt{\kwd{fn} \typ{<Nat>} x \kwd{=>} e} \\
                e \ e'                              &\mapsto               \texttt{e' e} \\
                (\lambda x : Nat . e )\ e'           &\mapsto               \texttt{\kwd{let} \typ{<Nat>} x \kwd{:=} e'; e} \\
                \Lambda X. e                        &\mapsto                \texttt{\typ{/{\char`\\} X.} e}\\
                e\ \forall X.X                      &\mapsto                \texttt{e \typ{<{\char`\\}/X.X>} }\\
                \text{letrec}_{Nat\to Nat}\ f = e    &\mapsto               \texttt{\kwd{letrec} \typ{<Nat->Nat>} f \kwd{:=} e}\\
                \text{case}_X\ e \text{ of } \{ c \Rightarrow e\} &\mapsto  \texttt{\kwd{case} \typ{<X>} e \kwd{of} \{c \kwd{=>} e\}} \\
                bind\ f\ e                             &\mapsto               \texttt{ \kwd{bind} f e} \\
                unit\ e                              &\mapsto                \texttt{ \kwd{unit} e} 
            \end{align*}
        \end{block}
    \end{frame}
    
    \begin{frame}
        \frametitle{Compilator}
        \begin{block}<+->{Generare de cod}
            \begin{itemize}
                \item \textit{TBT} $\mapsto$ \textit{Java}
                \item \^ Inchideri func\c tionale
                \item ANTLR + StringTemplate
            \end{itemize}
        \end{block}
        \begin{block}<+->{Typechecker}
            \begin{itemize}
            \item Variabile de inferen\c t\u a
            $$ s : Nat^{\av{3-}{3}{$v_1$}} \to Nat^{\av{3-}{3}{$\widehat{v_1}$}} ,
               z : Nat^{\av{3-}{3}{$\widehat{v_2}$}} \vdash 
               \lambda f : Nat^{\av{3-}{3}{$v_3$}} \to Nat^{\av{3-}{3}{$v_4$}} . f\ z : Nat^{\av{3-}{3}{$v_4$}}$$
            \item<4-> Constr\^ angeri \^ intre variabile $\Rightarrow$ clas\u a de tipuri
            $$ Nat^{\widehat{v_2}} \sqsubseteq Nat^{v_3} \Rightarrow \{\widehat{v_2} \le v_3 \}$$
            \end{itemize}
        \end{block}
    \end{frame}

%-----------------------------------------------------------------------------------
    \begin{frame}
    \setbeamercolor{qa}{fg=block title.fg,bg=block title.bg} %structure.fg

    \begin{beamercolorbox}[rounded=true,shadow=true]{qa}
    \begin{center}
        {\Huge \textbf{Mul\c tumesc!}}
    \end{center}
    \end{beamercolorbox}
    \vfill
    \begin{columns}
            \begin{column}[l]{0.5\textwidth}
                \begin{itemize}
                    \item Normalizare puternic\u a
                    \item Calcul Lambda
                    \item \^ Inchideri func\c tionale
                    \item ANTLR + StringTemplate
                \end{itemize}
            \end{column}
            \begin{column}[l]{0.5\textwidth}
                \begin{itemize}
                    \item (In)completitudine Turing
                    \item Sisteme de tipuri
                    \item Variabile de inferen\c t\u a
                    \item Constr\^ angeri
                \end{itemize}
            \end{column}
    \end{columns}
    \end{frame}

\end{document}
